\begin{tabbing}
$\forall$${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $m$:$\mathbb{N}$, $A$:ecl{-}trans{-}tuple\=\{i:l\}\+
\\[0ex](${\it ds}$; ${\it da}$).
\-\\[0ex]add{-}ecl{-}act($A$; $m$) $\in$ ecl{-}trans{-}tuple\{i:l\}(${\it ds}$; ${\it da}$)
\end{tabbing}